Termination of the given JBC could be proven:

0 JBC
↳1 JBC2FIG (⇐)
↳2 FIGraph
↳3 FIGtoITRSProof (⇐)
↳4 ITRS
↳5 DuplicateArgsRemoverProof (⇔)
↳6 ITRS
↳7 ITRStoIDPProof (⇔)
↳8 IDP
↳9 UsableRulesProof (⇔)
↳10 IDP
↳11 IDPNonInfProof (⇐)
↳12 AND
    ↳13 IDP
        ↳14 IDependencyGraphProof (⇔)
        ↳15 IDP
        ↳16 IDPNonInfProof (⇐)
        ↳17 AND
            ↳18 IDP
                ↳19 IDependencyGraphProof (⇔)
                ↳20 TRUE
            ↳21 IDP
                ↳22 IDependencyGraphProof (⇔)
                ↳23 TRUE
    ↳24 IDP
        ↳25 IDependencyGraphProof (⇔)
        ↳26 IDP
        ↳27 IDPNonInfProof (⇐)
        ↳28 AND
            ↳29 IDP
                ↳30 IDependencyGraphProof (⇔)
                ↳31 TRUE
            ↳32 IDP
                ↳33 IDependencyGraphProof (⇔)
                ↳34 TRUE

(0) Obligation:

JBC Problem based on JBC Program:
No human-readable program information known.

Manifest-Version: 1.0 Created-By: 1.6.0_16 (Sun Microsystems Inc.) Main-Class: PastaB15

(1) JBC2FIG (SOUND transformation)

Constructed FIGraph.

(2) Obligation:

FIGraph based on JBC Program:
Graph of 237 nodes with 1 SCC.

(3) FIGtoITRSProof (SOUND transformation)

Transformed FIGraph to ITRS rules

(4) Obligation:

ITRS problem:

The following function symbols are pre-defined:
!=~Neq: (Integer, Integer) -> Boolean
*~Mul: (Integer, Integer) -> Integer
>=~Ge: (Integer, Integer) -> Boolean
-1~UnaryMinus: (Integer) -> Integer
|~Bwor: (Integer, Integer) -> Integer
/~Div: (Integer, Integer) -> Integer
=~Eq: (Integer, Integer) -> Boolean
~Bwxor: (Integer, Integer) -> Integer
||~Lor: (Boolean, Boolean) -> Boolean
!~Lnot: (Boolean) -> Boolean
<~Lt: (Integer, Integer) -> Boolean
-~Sub: (Integer, Integer) -> Integer
<=~Le: (Integer, Integer) -> Boolean
>~Gt: (Integer, Integer) -> Boolean
~~Bwnot: (Integer) -> Integer
%~Mod: (Integer, Integer) -> Integer
&~Bwand: (Integer, Integer) -> Integer
+~Add: (Integer, Integer) -> Integer
&&~Land: (Boolean, Boolean) -> Boolean

The TRS R consists of the following rules:
Load1146(i112, i112, i84) → Cond_Load1146(i84 >= 0 && i112 > i84, i112, i112, i84)
Cond_Load1146(TRUE, i112, i112, i84) → Load1221(i112, i112, i84)
Load1221(i118, i119, i84) → Cond_Load1221(i84 >= 0 && i119 > i84, i118, i119, i84)
Cond_Load1221(TRUE, i118, i119, i84) → Load1221(i118 + -1, i119 + -1, i84)
Load1221(i118, i119, i84) → Cond_Load12211(i119 <= i84, i118, i119, i84)
Cond_Load12211(TRUE, i118, i119, i84) → Load1146(i118, i119, i84)
The set Q consists of the following terms:
Load1146(x0, x0, x1)
Cond_Load1146(TRUE, x0, x0, x1)
Load1221(x0, x1, x2)
Cond_Load1221(TRUE, x0, x1, x2)
Cond_Load12211(TRUE, x0, x1, x2)

(5) DuplicateArgsRemoverProof (EQUIVALENT transformation)

Some arguments are removed because they only appear as duplicates.
We removed arguments according to the following replacements:

Cond_Load1146(x1, x2, x3, x4) → Cond_Load1146(x1, x3, x4)

(6) Obligation:

ITRS problem:

The following function symbols are pre-defined:
!=~Neq: (Integer, Integer) -> Boolean
*~Mul: (Integer, Integer) -> Integer
>=~Ge: (Integer, Integer) -> Boolean
-1~UnaryMinus: (Integer) -> Integer
|~Bwor: (Integer, Integer) -> Integer
/~Div: (Integer, Integer) -> Integer
=~Eq: (Integer, Integer) -> Boolean
~Bwxor: (Integer, Integer) -> Integer
||~Lor: (Boolean, Boolean) -> Boolean
!~Lnot: (Boolean) -> Boolean
<~Lt: (Integer, Integer) -> Boolean
-~Sub: (Integer, Integer) -> Integer
<=~Le: (Integer, Integer) -> Boolean
>~Gt: (Integer, Integer) -> Boolean
~~Bwnot: (Integer) -> Integer
%~Mod: (Integer, Integer) -> Integer
&~Bwand: (Integer, Integer) -> Integer
+~Add: (Integer, Integer) -> Integer
&&~Land: (Boolean, Boolean) -> Boolean

The TRS R consists of the following rules:
Load1146(i112, i112, i84) → Cond_Load1146(i84 >= 0 && i112 > i84, i112, i84)
Cond_Load1146(TRUE, i112, i84) → Load1221(i112, i112, i84)
Load1221(i118, i119, i84) → Cond_Load1221(i84 >= 0 && i119 > i84, i118, i119, i84)
Cond_Load1221(TRUE, i118, i119, i84) → Load1221(i118 + -1, i119 + -1, i84)
Load1221(i118, i119, i84) → Cond_Load12211(i119 <= i84, i118, i119, i84)
Cond_Load12211(TRUE, i118, i119, i84) → Load1146(i118, i119, i84)
The set Q consists of the following terms:
Load1146(x0, x0, x1)
Cond_Load1146(TRUE, x0, x1)
Load1221(x0, x1, x2)
Cond_Load1221(TRUE, x0, x1, x2)
Cond_Load12211(TRUE, x0, x1, x2)

(7) ITRStoIDPProof (EQUIVALENT transformation)

Added dependency pairs

(8) Obligation:

IDP problem:
The following function symbols are pre-defined:
!=~Neq: (Integer, Integer) -> Boolean
*~Mul: (Integer, Integer) -> Integer
>=~Ge: (Integer, Integer) -> Boolean
-1~UnaryMinus: (Integer) -> Integer
|~Bwor: (Integer, Integer) -> Integer
/~Div: (Integer, Integer) -> Integer
=~Eq: (Integer, Integer) -> Boolean
~Bwxor: (Integer, Integer) -> Integer
||~Lor: (Boolean, Boolean) -> Boolean
!~Lnot: (Boolean) -> Boolean
<~Lt: (Integer, Integer) -> Boolean
-~Sub: (Integer, Integer) -> Integer
<=~Le: (Integer, Integer) -> Boolean
>~Gt: (Integer, Integer) -> Boolean
~~Bwnot: (Integer) -> Integer
%~Mod: (Integer, Integer) -> Integer
&~Bwand: (Integer, Integer) -> Integer
+~Add: (Integer, Integer) -> Integer
&&~Land: (Boolean, Boolean) -> Boolean


The following domains are used:

Boolean, Integer


The ITRS R consists of the following rules:
Load1146(i112, i112, i84) → Cond_Load1146(i84 >= 0 && i112 > i84, i112, i84)
Cond_Load1146(TRUE, i112, i84) → Load1221(i112, i112, i84)
Load1221(i118, i119, i84) → Cond_Load1221(i84 >= 0 && i119 > i84, i118, i119, i84)
Cond_Load1221(TRUE, i118, i119, i84) → Load1221(i118 + -1, i119 + -1, i84)
Load1221(i118, i119, i84) → Cond_Load12211(i119 <= i84, i118, i119, i84)
Cond_Load12211(TRUE, i118, i119, i84) → Load1146(i118, i119, i84)

The integer pair graph contains the following rules and edges:
(0): LOAD1146(i112[0], i112[0], i84[0]) → COND_LOAD1146(i84[0] >= 0 && i112[0] > i84[0], i112[0], i84[0])
(1): COND_LOAD1146(TRUE, i112[1], i84[1]) → LOAD1221(i112[1], i112[1], i84[1])
(2): LOAD1221(i118[2], i119[2], i84[2]) → COND_LOAD1221(i84[2] >= 0 && i119[2] > i84[2], i118[2], i119[2], i84[2])
(3): COND_LOAD1221(TRUE, i118[3], i119[3], i84[3]) → LOAD1221(i118[3] + -1, i119[3] + -1, i84[3])
(4): LOAD1221(i118[4], i119[4], i84[4]) → COND_LOAD12211(i119[4] <= i84[4], i118[4], i119[4], i84[4])
(5): COND_LOAD12211(TRUE, i118[5], i119[5], i84[5]) → LOAD1146(i118[5], i119[5], i84[5])

(0) -> (1), if ((i112[0] →* i112[1])∧(i84[0] >= 0 && i112[0] > i84[0] →* TRUE)∧(i84[0] →* i84[1]))


(1) -> (2), if ((i112[1] →* i118[2])∧(i112[1] →* i119[2])∧(i84[1] →* i84[2]))


(1) -> (4), if ((i112[1] →* i119[4])∧(i112[1] →* i118[4])∧(i84[1] →* i84[4]))


(2) -> (3), if ((i84[2] >= 0 && i119[2] > i84[2] →* TRUE)∧(i119[2] →* i119[3])∧(i84[2] →* i84[3])∧(i118[2] →* i118[3]))


(3) -> (2), if ((i119[3] + -1 →* i119[2])∧(i118[3] + -1 →* i118[2])∧(i84[3] →* i84[2]))


(3) -> (4), if ((i84[3] →* i84[4])∧(i119[3] + -1 →* i119[4])∧(i118[3] + -1 →* i118[4]))


(4) -> (5), if ((i119[4] →* i119[5])∧(i84[4] →* i84[5])∧(i118[4] →* i118[5])∧(i119[4] <= i84[4] →* TRUE))


(5) -> (0), if ((i118[5] →* i112[0])∧(i84[5] →* i84[0])∧(i119[5] →* i112[0]))



The set Q consists of the following terms:
Load1146(x0, x0, x1)
Cond_Load1146(TRUE, x0, x1)
Load1221(x0, x1, x2)
Cond_Load1221(TRUE, x0, x1, x2)
Cond_Load12211(TRUE, x0, x1, x2)

(9) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(10) Obligation:

IDP problem:
The following function symbols are pre-defined:
!=~Neq: (Integer, Integer) -> Boolean
*~Mul: (Integer, Integer) -> Integer
>=~Ge: (Integer, Integer) -> Boolean
-1~UnaryMinus: (Integer) -> Integer
|~Bwor: (Integer, Integer) -> Integer
/~Div: (Integer, Integer) -> Integer
=~Eq: (Integer, Integer) -> Boolean
~Bwxor: (Integer, Integer) -> Integer
||~Lor: (Boolean, Boolean) -> Boolean
!~Lnot: (Boolean) -> Boolean
<~Lt: (Integer, Integer) -> Boolean
-~Sub: (Integer, Integer) -> Integer
<=~Le: (Integer, Integer) -> Boolean
>~Gt: (Integer, Integer) -> Boolean
~~Bwnot: (Integer) -> Integer
%~Mod: (Integer, Integer) -> Integer
&~Bwand: (Integer, Integer) -> Integer
+~Add: (Integer, Integer) -> Integer
&&~Land: (Boolean, Boolean) -> Boolean


The following domains are used:

Boolean, Integer


R is empty.

The integer pair graph contains the following rules and edges:
(0): LOAD1146(i112[0], i112[0], i84[0]) → COND_LOAD1146(i84[0] >= 0 && i112[0] > i84[0], i112[0], i84[0])
(1): COND_LOAD1146(TRUE, i112[1], i84[1]) → LOAD1221(i112[1], i112[1], i84[1])
(2): LOAD1221(i118[2], i119[2], i84[2]) → COND_LOAD1221(i84[2] >= 0 && i119[2] > i84[2], i118[2], i119[2], i84[2])
(3): COND_LOAD1221(TRUE, i118[3], i119[3], i84[3]) → LOAD1221(i118[3] + -1, i119[3] + -1, i84[3])
(4): LOAD1221(i118[4], i119[4], i84[4]) → COND_LOAD12211(i119[4] <= i84[4], i118[4], i119[4], i84[4])
(5): COND_LOAD12211(TRUE, i118[5], i119[5], i84[5]) → LOAD1146(i118[5], i119[5], i84[5])

(0) -> (1), if ((i112[0] →* i112[1])∧(i84[0] >= 0 && i112[0] > i84[0] →* TRUE)∧(i84[0] →* i84[1]))


(1) -> (2), if ((i112[1] →* i118[2])∧(i112[1] →* i119[2])∧(i84[1] →* i84[2]))


(1) -> (4), if ((i112[1] →* i119[4])∧(i112[1] →* i118[4])∧(i84[1] →* i84[4]))


(2) -> (3), if ((i84[2] >= 0 && i119[2] > i84[2] →* TRUE)∧(i119[2] →* i119[3])∧(i84[2] →* i84[3])∧(i118[2] →* i118[3]))


(3) -> (2), if ((i119[3] + -1 →* i119[2])∧(i118[3] + -1 →* i118[2])∧(i84[3] →* i84[2]))


(3) -> (4), if ((i84[3] →* i84[4])∧(i119[3] + -1 →* i119[4])∧(i118[3] + -1 →* i118[4]))


(4) -> (5), if ((i119[4] →* i119[5])∧(i84[4] →* i84[5])∧(i118[4] →* i118[5])∧(i119[4] <= i84[4] →* TRUE))


(5) -> (0), if ((i118[5] →* i112[0])∧(i84[5] →* i84[0])∧(i119[5] →* i112[0]))



The set Q consists of the following terms:
Load1146(x0, x0, x1)
Cond_Load1146(TRUE, x0, x1)
Load1221(x0, x1, x2)
Cond_Load1221(TRUE, x0, x1, x2)
Cond_Load12211(TRUE, x0, x1, x2)

(11) IDPNonInfProof (SOUND transformation)

The constraints were generated the following way:
The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that final constraints are written in bold face.


For Pair LOAD1146(i112, i112, i84) → COND_LOAD1146(&&(>=(i84, 0), >(i112, i84)), i112, i84) the following chains were created:
  • We consider the chain LOAD1146(i112[0], i112[0], i84[0]) → COND_LOAD1146(&&(>=(i84[0], 0), >(i112[0], i84[0])), i112[0], i84[0]), COND_LOAD1146(TRUE, i112[1], i84[1]) → LOAD1221(i112[1], i112[1], i84[1]) which results in the following constraint:

    (1)    (i112[0]=i112[1]∧&&(>=(i84[0], 0), >(i112[0], i84[0]))=TRUE∧i84[0]=i84[1] ⇒ LOAD1146(i112[0], i112[0], i84[0])≥NonInfC∧LOAD1146(i112[0], i112[0], i84[0])≥COND_LOAD1146(&&(>=(i84[0], 0), >(i112[0], i84[0])), i112[0], i84[0])∧(UIncreasing(COND_LOAD1146(&&(>=(i84[0], 0), >(i112[0], i84[0])), i112[0], i84[0])), ≥))



    We simplified constraint (1) using rules (IV), (IDP_BOOLEAN) which results in the following new constraint:

    (2)    (>=(i84[0], 0)=TRUE∧>(i112[0], i84[0])=TRUE ⇒ LOAD1146(i112[0], i112[0], i84[0])≥NonInfC∧LOAD1146(i112[0], i112[0], i84[0])≥COND_LOAD1146(&&(>=(i84[0], 0), >(i112[0], i84[0])), i112[0], i84[0])∧(UIncreasing(COND_LOAD1146(&&(>=(i84[0], 0), >(i112[0], i84[0])), i112[0], i84[0])), ≥))



    We simplified constraint (2) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (3)    (i84[0] ≥ 0∧i112[0] + [-1] + [-1]i84[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1146(&&(>=(i84[0], 0), >(i112[0], i84[0])), i112[0], i84[0])), ≥)∧[(-1)bni_29 + (-1)Bound*bni_29] + [(-1)bni_29]i84[0] + [bni_29]i112[0] ≥ 0∧[(-1)bso_30] ≥ 0)



    We simplified constraint (3) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (4)    (i84[0] ≥ 0∧i112[0] + [-1] + [-1]i84[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1146(&&(>=(i84[0], 0), >(i112[0], i84[0])), i112[0], i84[0])), ≥)∧[(-1)bni_29 + (-1)Bound*bni_29] + [(-1)bni_29]i84[0] + [bni_29]i112[0] ≥ 0∧[(-1)bso_30] ≥ 0)



    We simplified constraint (4) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (5)    (i84[0] ≥ 0∧i112[0] + [-1] + [-1]i84[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1146(&&(>=(i84[0], 0), >(i112[0], i84[0])), i112[0], i84[0])), ≥)∧[(-1)bni_29 + (-1)Bound*bni_29] + [(-1)bni_29]i84[0] + [bni_29]i112[0] ≥ 0∧[(-1)bso_30] ≥ 0)



    We simplified constraint (5) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (6)    (i84[0] ≥ 0∧i112[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1146(&&(>=(i84[0], 0), >(i112[0], i84[0])), i112[0], i84[0])), ≥)∧[(-1)Bound*bni_29] + [bni_29]i112[0] ≥ 0∧[(-1)bso_30] ≥ 0)







For Pair COND_LOAD1146(TRUE, i112, i84) → LOAD1221(i112, i112, i84) the following chains were created:
  • We consider the chain COND_LOAD1146(TRUE, i112[1], i84[1]) → LOAD1221(i112[1], i112[1], i84[1]), LOAD1221(i118[2], i119[2], i84[2]) → COND_LOAD1221(&&(>=(i84[2], 0), >(i119[2], i84[2])), i118[2], i119[2], i84[2]) which results in the following constraint:

    (7)    (i112[1]=i118[2]∧i112[1]=i119[2]∧i84[1]=i84[2] ⇒ COND_LOAD1146(TRUE, i112[1], i84[1])≥NonInfC∧COND_LOAD1146(TRUE, i112[1], i84[1])≥LOAD1221(i112[1], i112[1], i84[1])∧(UIncreasing(LOAD1221(i112[1], i112[1], i84[1])), ≥))



    We simplified constraint (7) using rule (IV) which results in the following new constraint:

    (8)    (COND_LOAD1146(TRUE, i112[1], i84[1])≥NonInfC∧COND_LOAD1146(TRUE, i112[1], i84[1])≥LOAD1221(i112[1], i112[1], i84[1])∧(UIncreasing(LOAD1221(i112[1], i112[1], i84[1])), ≥))



    We simplified constraint (8) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (9)    ((UIncreasing(LOAD1221(i112[1], i112[1], i84[1])), ≥)∧[(-1)bso_32] ≥ 0)



    We simplified constraint (9) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (10)    ((UIncreasing(LOAD1221(i112[1], i112[1], i84[1])), ≥)∧[(-1)bso_32] ≥ 0)



    We simplified constraint (10) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (11)    ((UIncreasing(LOAD1221(i112[1], i112[1], i84[1])), ≥)∧[(-1)bso_32] ≥ 0)



    We simplified constraint (11) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

    (12)    ((UIncreasing(LOAD1221(i112[1], i112[1], i84[1])), ≥)∧0 = 0∧0 = 0∧[(-1)bso_32] ≥ 0)



  • We consider the chain COND_LOAD1146(TRUE, i112[1], i84[1]) → LOAD1221(i112[1], i112[1], i84[1]), LOAD1221(i118[4], i119[4], i84[4]) → COND_LOAD12211(<=(i119[4], i84[4]), i118[4], i119[4], i84[4]) which results in the following constraint:

    (13)    (i112[1]=i119[4]∧i112[1]=i118[4]∧i84[1]=i84[4] ⇒ COND_LOAD1146(TRUE, i112[1], i84[1])≥NonInfC∧COND_LOAD1146(TRUE, i112[1], i84[1])≥LOAD1221(i112[1], i112[1], i84[1])∧(UIncreasing(LOAD1221(i112[1], i112[1], i84[1])), ≥))



    We simplified constraint (13) using rule (IV) which results in the following new constraint:

    (14)    (COND_LOAD1146(TRUE, i112[1], i84[1])≥NonInfC∧COND_LOAD1146(TRUE, i112[1], i84[1])≥LOAD1221(i112[1], i112[1], i84[1])∧(UIncreasing(LOAD1221(i112[1], i112[1], i84[1])), ≥))



    We simplified constraint (14) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (15)    ((UIncreasing(LOAD1221(i112[1], i112[1], i84[1])), ≥)∧[(-1)bso_32] ≥ 0)



    We simplified constraint (15) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (16)    ((UIncreasing(LOAD1221(i112[1], i112[1], i84[1])), ≥)∧[(-1)bso_32] ≥ 0)



    We simplified constraint (16) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (17)    ((UIncreasing(LOAD1221(i112[1], i112[1], i84[1])), ≥)∧[(-1)bso_32] ≥ 0)



    We simplified constraint (17) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

    (18)    ((UIncreasing(LOAD1221(i112[1], i112[1], i84[1])), ≥)∧0 = 0∧0 = 0∧[(-1)bso_32] ≥ 0)







For Pair LOAD1221(i118, i119, i84) → COND_LOAD1221(&&(>=(i84, 0), >(i119, i84)), i118, i119, i84) the following chains were created:
  • We consider the chain LOAD1221(i118[2], i119[2], i84[2]) → COND_LOAD1221(&&(>=(i84[2], 0), >(i119[2], i84[2])), i118[2], i119[2], i84[2]), COND_LOAD1221(TRUE, i118[3], i119[3], i84[3]) → LOAD1221(+(i118[3], -1), +(i119[3], -1), i84[3]) which results in the following constraint:

    (19)    (&&(>=(i84[2], 0), >(i119[2], i84[2]))=TRUE∧i119[2]=i119[3]∧i84[2]=i84[3]∧i118[2]=i118[3] ⇒ LOAD1221(i118[2], i119[2], i84[2])≥NonInfC∧LOAD1221(i118[2], i119[2], i84[2])≥COND_LOAD1221(&&(>=(i84[2], 0), >(i119[2], i84[2])), i118[2], i119[2], i84[2])∧(UIncreasing(COND_LOAD1221(&&(>=(i84[2], 0), >(i119[2], i84[2])), i118[2], i119[2], i84[2])), ≥))



    We simplified constraint (19) using rules (IV), (IDP_BOOLEAN) which results in the following new constraint:

    (20)    (>=(i84[2], 0)=TRUE∧>(i119[2], i84[2])=TRUE ⇒ LOAD1221(i118[2], i119[2], i84[2])≥NonInfC∧LOAD1221(i118[2], i119[2], i84[2])≥COND_LOAD1221(&&(>=(i84[2], 0), >(i119[2], i84[2])), i118[2], i119[2], i84[2])∧(UIncreasing(COND_LOAD1221(&&(>=(i84[2], 0), >(i119[2], i84[2])), i118[2], i119[2], i84[2])), ≥))



    We simplified constraint (20) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (21)    (i84[2] ≥ 0∧i119[2] + [-1] + [-1]i84[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1221(&&(>=(i84[2], 0), >(i119[2], i84[2])), i118[2], i119[2], i84[2])), ≥)∧[(-1)bni_33 + (-1)Bound*bni_33] + [(-1)bni_33]i84[2] + [(-1)bni_33]i119[2] + [(2)bni_33]i118[2] ≥ 0∧[(-1)bso_34] ≥ 0)



    We simplified constraint (21) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (22)    (i84[2] ≥ 0∧i119[2] + [-1] + [-1]i84[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1221(&&(>=(i84[2], 0), >(i119[2], i84[2])), i118[2], i119[2], i84[2])), ≥)∧[(-1)bni_33 + (-1)Bound*bni_33] + [(-1)bni_33]i84[2] + [(-1)bni_33]i119[2] + [(2)bni_33]i118[2] ≥ 0∧[(-1)bso_34] ≥ 0)



    We simplified constraint (22) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (23)    (i84[2] ≥ 0∧i119[2] + [-1] + [-1]i84[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1221(&&(>=(i84[2], 0), >(i119[2], i84[2])), i118[2], i119[2], i84[2])), ≥)∧[(-1)bni_33 + (-1)Bound*bni_33] + [(-1)bni_33]i84[2] + [(-1)bni_33]i119[2] + [(2)bni_33]i118[2] ≥ 0∧[(-1)bso_34] ≥ 0)



    We simplified constraint (23) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

    (24)    (i84[2] ≥ 0∧i119[2] + [-1] + [-1]i84[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1221(&&(>=(i84[2], 0), >(i119[2], i84[2])), i118[2], i119[2], i84[2])), ≥)∧[(2)bni_33] = 0∧[(-1)bni_33 + (-1)Bound*bni_33] + [(-1)bni_33]i84[2] + [(-1)bni_33]i119[2] ≥ 0∧0 = 0∧[(-1)bso_34] ≥ 0)



    We simplified constraint (24) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (25)    (i84[2] ≥ 0∧i119[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1221(&&(>=(i84[2], 0), >(i119[2], i84[2])), i118[2], i119[2], i84[2])), ≥)∧[(2)bni_33] = 0∧[(-2)bni_33 + (-1)Bound*bni_33] + [(-2)bni_33]i84[2] + [(-1)bni_33]i119[2] ≥ 0∧0 = 0∧[(-1)bso_34] ≥ 0)







For Pair COND_LOAD1221(TRUE, i118, i119, i84) → LOAD1221(+(i118, -1), +(i119, -1), i84) the following chains were created:
  • We consider the chain LOAD1221(i118[2], i119[2], i84[2]) → COND_LOAD1221(&&(>=(i84[2], 0), >(i119[2], i84[2])), i118[2], i119[2], i84[2]), COND_LOAD1221(TRUE, i118[3], i119[3], i84[3]) → LOAD1221(+(i118[3], -1), +(i119[3], -1), i84[3]), LOAD1221(i118[2], i119[2], i84[2]) → COND_LOAD1221(&&(>=(i84[2], 0), >(i119[2], i84[2])), i118[2], i119[2], i84[2]) which results in the following constraint:

    (26)    (&&(>=(i84[2], 0), >(i119[2], i84[2]))=TRUE∧i119[2]=i119[3]∧i84[2]=i84[3]∧i118[2]=i118[3]∧+(i119[3], -1)=i119[2]1∧+(i118[3], -1)=i118[2]1∧i84[3]=i84[2]1 ⇒ COND_LOAD1221(TRUE, i118[3], i119[3], i84[3])≥NonInfC∧COND_LOAD1221(TRUE, i118[3], i119[3], i84[3])≥LOAD1221(+(i118[3], -1), +(i119[3], -1), i84[3])∧(UIncreasing(LOAD1221(+(i118[3], -1), +(i119[3], -1), i84[3])), ≥))



    We simplified constraint (26) using rules (III), (IV), (IDP_BOOLEAN) which results in the following new constraint:

    (27)    (>=(i84[2], 0)=TRUE∧>(i119[2], i84[2])=TRUE ⇒ COND_LOAD1221(TRUE, i118[2], i119[2], i84[2])≥NonInfC∧COND_LOAD1221(TRUE, i118[2], i119[2], i84[2])≥LOAD1221(+(i118[2], -1), +(i119[2], -1), i84[2])∧(UIncreasing(LOAD1221(+(i118[3], -1), +(i119[3], -1), i84[3])), ≥))



    We simplified constraint (27) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (28)    (i84[2] ≥ 0∧i119[2] + [-1] + [-1]i84[2] ≥ 0 ⇒ (UIncreasing(LOAD1221(+(i118[3], -1), +(i119[3], -1), i84[3])), ≥)∧[(-1)bni_35 + (-1)Bound*bni_35] + [(-1)bni_35]i84[2] + [(-1)bni_35]i119[2] + [(2)bni_35]i118[2] ≥ 0∧[1 + (-1)bso_36] ≥ 0)



    We simplified constraint (28) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (29)    (i84[2] ≥ 0∧i119[2] + [-1] + [-1]i84[2] ≥ 0 ⇒ (UIncreasing(LOAD1221(+(i118[3], -1), +(i119[3], -1), i84[3])), ≥)∧[(-1)bni_35 + (-1)Bound*bni_35] + [(-1)bni_35]i84[2] + [(-1)bni_35]i119[2] + [(2)bni_35]i118[2] ≥ 0∧[1 + (-1)bso_36] ≥ 0)



    We simplified constraint (29) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (30)    (i84[2] ≥ 0∧i119[2] + [-1] + [-1]i84[2] ≥ 0 ⇒ (UIncreasing(LOAD1221(+(i118[3], -1), +(i119[3], -1), i84[3])), ≥)∧[(-1)bni_35 + (-1)Bound*bni_35] + [(-1)bni_35]i84[2] + [(-1)bni_35]i119[2] + [(2)bni_35]i118[2] ≥ 0∧[1 + (-1)bso_36] ≥ 0)



    We simplified constraint (30) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

    (31)    (i84[2] ≥ 0∧i119[2] + [-1] + [-1]i84[2] ≥ 0 ⇒ (UIncreasing(LOAD1221(+(i118[3], -1), +(i119[3], -1), i84[3])), ≥)∧[(2)bni_35] = 0∧[(-1)bni_35 + (-1)Bound*bni_35] + [(-1)bni_35]i84[2] + [(-1)bni_35]i119[2] ≥ 0∧0 = 0∧[1 + (-1)bso_36] ≥ 0)



    We simplified constraint (31) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (32)    (i84[2] ≥ 0∧i119[2] ≥ 0 ⇒ (UIncreasing(LOAD1221(+(i118[3], -1), +(i119[3], -1), i84[3])), ≥)∧[(2)bni_35] = 0∧[(-2)bni_35 + (-1)Bound*bni_35] + [(-2)bni_35]i84[2] + [(-1)bni_35]i119[2] ≥ 0∧0 = 0∧[1 + (-1)bso_36] ≥ 0)



  • We consider the chain LOAD1221(i118[2], i119[2], i84[2]) → COND_LOAD1221(&&(>=(i84[2], 0), >(i119[2], i84[2])), i118[2], i119[2], i84[2]), COND_LOAD1221(TRUE, i118[3], i119[3], i84[3]) → LOAD1221(+(i118[3], -1), +(i119[3], -1), i84[3]), LOAD1221(i118[4], i119[4], i84[4]) → COND_LOAD12211(<=(i119[4], i84[4]), i118[4], i119[4], i84[4]) which results in the following constraint:

    (33)    (&&(>=(i84[2], 0), >(i119[2], i84[2]))=TRUE∧i119[2]=i119[3]∧i84[2]=i84[3]∧i118[2]=i118[3]∧i84[3]=i84[4]∧+(i119[3], -1)=i119[4]∧+(i118[3], -1)=i118[4] ⇒ COND_LOAD1221(TRUE, i118[3], i119[3], i84[3])≥NonInfC∧COND_LOAD1221(TRUE, i118[3], i119[3], i84[3])≥LOAD1221(+(i118[3], -1), +(i119[3], -1), i84[3])∧(UIncreasing(LOAD1221(+(i118[3], -1), +(i119[3], -1), i84[3])), ≥))



    We simplified constraint (33) using rules (III), (IV), (IDP_BOOLEAN) which results in the following new constraint:

    (34)    (>=(i84[2], 0)=TRUE∧>(i119[2], i84[2])=TRUE ⇒ COND_LOAD1221(TRUE, i118[2], i119[2], i84[2])≥NonInfC∧COND_LOAD1221(TRUE, i118[2], i119[2], i84[2])≥LOAD1221(+(i118[2], -1), +(i119[2], -1), i84[2])∧(UIncreasing(LOAD1221(+(i118[3], -1), +(i119[3], -1), i84[3])), ≥))



    We simplified constraint (34) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (35)    (i84[2] ≥ 0∧i119[2] + [-1] + [-1]i84[2] ≥ 0 ⇒ (UIncreasing(LOAD1221(+(i118[3], -1), +(i119[3], -1), i84[3])), ≥)∧[(-1)bni_35 + (-1)Bound*bni_35] + [(-1)bni_35]i84[2] + [(-1)bni_35]i119[2] + [(2)bni_35]i118[2] ≥ 0∧[1 + (-1)bso_36] ≥ 0)



    We simplified constraint (35) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (36)    (i84[2] ≥ 0∧i119[2] + [-1] + [-1]i84[2] ≥ 0 ⇒ (UIncreasing(LOAD1221(+(i118[3], -1), +(i119[3], -1), i84[3])), ≥)∧[(-1)bni_35 + (-1)Bound*bni_35] + [(-1)bni_35]i84[2] + [(-1)bni_35]i119[2] + [(2)bni_35]i118[2] ≥ 0∧[1 + (-1)bso_36] ≥ 0)



    We simplified constraint (36) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (37)    (i84[2] ≥ 0∧i119[2] + [-1] + [-1]i84[2] ≥ 0 ⇒ (UIncreasing(LOAD1221(+(i118[3], -1), +(i119[3], -1), i84[3])), ≥)∧[(-1)bni_35 + (-1)Bound*bni_35] + [(-1)bni_35]i84[2] + [(-1)bni_35]i119[2] + [(2)bni_35]i118[2] ≥ 0∧[1 + (-1)bso_36] ≥ 0)



    We simplified constraint (37) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

    (38)    (i84[2] ≥ 0∧i119[2] + [-1] + [-1]i84[2] ≥ 0 ⇒ (UIncreasing(LOAD1221(+(i118[3], -1), +(i119[3], -1), i84[3])), ≥)∧[(2)bni_35] = 0∧[(-1)bni_35 + (-1)Bound*bni_35] + [(-1)bni_35]i84[2] + [(-1)bni_35]i119[2] ≥ 0∧0 = 0∧[1 + (-1)bso_36] ≥ 0)



    We simplified constraint (38) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (39)    (i84[2] ≥ 0∧i119[2] ≥ 0 ⇒ (UIncreasing(LOAD1221(+(i118[3], -1), +(i119[3], -1), i84[3])), ≥)∧[(2)bni_35] = 0∧[(-2)bni_35 + (-1)Bound*bni_35] + [(-2)bni_35]i84[2] + [(-1)bni_35]i119[2] ≥ 0∧0 = 0∧[1 + (-1)bso_36] ≥ 0)







For Pair LOAD1221(i118, i119, i84) → COND_LOAD12211(<=(i119, i84), i118, i119, i84) the following chains were created:
  • We consider the chain LOAD1221(i118[4], i119[4], i84[4]) → COND_LOAD12211(<=(i119[4], i84[4]), i118[4], i119[4], i84[4]), COND_LOAD12211(TRUE, i118[5], i119[5], i84[5]) → LOAD1146(i118[5], i119[5], i84[5]) which results in the following constraint:

    (40)    (i119[4]=i119[5]∧i84[4]=i84[5]∧i118[4]=i118[5]∧<=(i119[4], i84[4])=TRUE ⇒ LOAD1221(i118[4], i119[4], i84[4])≥NonInfC∧LOAD1221(i118[4], i119[4], i84[4])≥COND_LOAD12211(<=(i119[4], i84[4]), i118[4], i119[4], i84[4])∧(UIncreasing(COND_LOAD12211(<=(i119[4], i84[4]), i118[4], i119[4], i84[4])), ≥))



    We simplified constraint (40) using rule (IV) which results in the following new constraint:

    (41)    (<=(i119[4], i84[4])=TRUE ⇒ LOAD1221(i118[4], i119[4], i84[4])≥NonInfC∧LOAD1221(i118[4], i119[4], i84[4])≥COND_LOAD12211(<=(i119[4], i84[4]), i118[4], i119[4], i84[4])∧(UIncreasing(COND_LOAD12211(<=(i119[4], i84[4]), i118[4], i119[4], i84[4])), ≥))



    We simplified constraint (41) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (42)    (i84[4] + [-1]i119[4] ≥ 0 ⇒ (UIncreasing(COND_LOAD12211(<=(i119[4], i84[4]), i118[4], i119[4], i84[4])), ≥)∧[(-1)bni_37 + (-1)Bound*bni_37] + [(-1)bni_37]i84[4] + [(-1)bni_37]i119[4] + [(2)bni_37]i118[4] ≥ 0∧[(-1)bso_38] ≥ 0)



    We simplified constraint (42) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (43)    (i84[4] + [-1]i119[4] ≥ 0 ⇒ (UIncreasing(COND_LOAD12211(<=(i119[4], i84[4]), i118[4], i119[4], i84[4])), ≥)∧[(-1)bni_37 + (-1)Bound*bni_37] + [(-1)bni_37]i84[4] + [(-1)bni_37]i119[4] + [(2)bni_37]i118[4] ≥ 0∧[(-1)bso_38] ≥ 0)



    We simplified constraint (43) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (44)    (i84[4] + [-1]i119[4] ≥ 0 ⇒ (UIncreasing(COND_LOAD12211(<=(i119[4], i84[4]), i118[4], i119[4], i84[4])), ≥)∧[(-1)bni_37 + (-1)Bound*bni_37] + [(-1)bni_37]i84[4] + [(-1)bni_37]i119[4] + [(2)bni_37]i118[4] ≥ 0∧[(-1)bso_38] ≥ 0)



    We simplified constraint (44) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

    (45)    (i84[4] + [-1]i119[4] ≥ 0 ⇒ (UIncreasing(COND_LOAD12211(<=(i119[4], i84[4]), i118[4], i119[4], i84[4])), ≥)∧[(2)bni_37] = 0∧[(-1)bni_37 + (-1)Bound*bni_37] + [(-1)bni_37]i84[4] + [(-1)bni_37]i119[4] ≥ 0∧0 = 0∧[(-1)bso_38] ≥ 0)



    We simplified constraint (45) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (46)    (i84[4] ≥ 0 ⇒ (UIncreasing(COND_LOAD12211(<=(i119[4], i84[4]), i118[4], i119[4], i84[4])), ≥)∧[(2)bni_37] = 0∧[(-1)bni_37 + (-1)Bound*bni_37] + [(-2)bni_37]i119[4] + [(-1)bni_37]i84[4] ≥ 0∧0 = 0∧[(-1)bso_38] ≥ 0)



    We simplified constraint (46) using rule (IDP_SMT_SPLIT) which results in the following new constraints:

    (47)    (i84[4] ≥ 0∧i119[4] ≥ 0 ⇒ (UIncreasing(COND_LOAD12211(<=(i119[4], i84[4]), i118[4], i119[4], i84[4])), ≥)∧[(2)bni_37] = 0∧[(-1)bni_37 + (-1)Bound*bni_37] + [(-2)bni_37]i119[4] + [(-1)bni_37]i84[4] ≥ 0∧0 = 0∧[(-1)bso_38] ≥ 0)


    (48)    (i84[4] ≥ 0∧i119[4] ≥ 0 ⇒ (UIncreasing(COND_LOAD12211(<=(i119[4], i84[4]), i118[4], i119[4], i84[4])), ≥)∧[(2)bni_37] = 0∧[(-1)bni_37 + (-1)Bound*bni_37] + [(2)bni_37]i119[4] + [(-1)bni_37]i84[4] ≥ 0∧0 = 0∧[(-1)bso_38] ≥ 0)







For Pair COND_LOAD12211(TRUE, i118, i119, i84) → LOAD1146(i118, i119, i84) the following chains were created:
  • We consider the chain COND_LOAD12211(TRUE, i118[5], i119[5], i84[5]) → LOAD1146(i118[5], i119[5], i84[5]), LOAD1146(i112[0], i112[0], i84[0]) → COND_LOAD1146(&&(>=(i84[0], 0), >(i112[0], i84[0])), i112[0], i84[0]) which results in the following constraint:

    (49)    (i118[5]=i112[0]∧i84[5]=i84[0]∧i119[5]=i112[0] ⇒ COND_LOAD12211(TRUE, i118[5], i119[5], i84[5])≥NonInfC∧COND_LOAD12211(TRUE, i118[5], i119[5], i84[5])≥LOAD1146(i118[5], i119[5], i84[5])∧(UIncreasing(LOAD1146(i118[5], i119[5], i84[5])), ≥))



    We simplified constraint (49) using rules (III), (IV) which results in the following new constraint:

    (50)    (COND_LOAD12211(TRUE, i119[5], i119[5], i84[5])≥NonInfC∧COND_LOAD12211(TRUE, i119[5], i119[5], i84[5])≥LOAD1146(i119[5], i119[5], i84[5])∧(UIncreasing(LOAD1146(i118[5], i119[5], i84[5])), ≥))



    We simplified constraint (50) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (51)    ((UIncreasing(LOAD1146(i118[5], i119[5], i84[5])), ≥)∧[(-1)bso_40] ≥ 0)



    We simplified constraint (51) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (52)    ((UIncreasing(LOAD1146(i118[5], i119[5], i84[5])), ≥)∧[(-1)bso_40] ≥ 0)



    We simplified constraint (52) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (53)    ((UIncreasing(LOAD1146(i118[5], i119[5], i84[5])), ≥)∧[(-1)bso_40] ≥ 0)



    We simplified constraint (53) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

    (54)    ((UIncreasing(LOAD1146(i118[5], i119[5], i84[5])), ≥)∧0 = 0∧0 = 0∧[(-1)bso_40] ≥ 0)







To summarize, we get the following constraints P≥ for the following pairs.
  • LOAD1146(i112, i112, i84) → COND_LOAD1146(&&(>=(i84, 0), >(i112, i84)), i112, i84)
    • (i84[0] ≥ 0∧i112[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1146(&&(>=(i84[0], 0), >(i112[0], i84[0])), i112[0], i84[0])), ≥)∧[(-1)Bound*bni_29] + [bni_29]i112[0] ≥ 0∧[(-1)bso_30] ≥ 0)

  • COND_LOAD1146(TRUE, i112, i84) → LOAD1221(i112, i112, i84)
    • ((UIncreasing(LOAD1221(i112[1], i112[1], i84[1])), ≥)∧0 = 0∧0 = 0∧[(-1)bso_32] ≥ 0)
    • ((UIncreasing(LOAD1221(i112[1], i112[1], i84[1])), ≥)∧0 = 0∧0 = 0∧[(-1)bso_32] ≥ 0)

  • LOAD1221(i118, i119, i84) → COND_LOAD1221(&&(>=(i84, 0), >(i119, i84)), i118, i119, i84)
    • (i84[2] ≥ 0∧i119[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1221(&&(>=(i84[2], 0), >(i119[2], i84[2])), i118[2], i119[2], i84[2])), ≥)∧[(2)bni_33] = 0∧[(-2)bni_33 + (-1)Bound*bni_33] + [(-2)bni_33]i84[2] + [(-1)bni_33]i119[2] ≥ 0∧0 = 0∧[(-1)bso_34] ≥ 0)

  • COND_LOAD1221(TRUE, i118, i119, i84) → LOAD1221(+(i118, -1), +(i119, -1), i84)
    • (i84[2] ≥ 0∧i119[2] ≥ 0 ⇒ (UIncreasing(LOAD1221(+(i118[3], -1), +(i119[3], -1), i84[3])), ≥)∧[(2)bni_35] = 0∧[(-2)bni_35 + (-1)Bound*bni_35] + [(-2)bni_35]i84[2] + [(-1)bni_35]i119[2] ≥ 0∧0 = 0∧[1 + (-1)bso_36] ≥ 0)
    • (i84[2] ≥ 0∧i119[2] ≥ 0 ⇒ (UIncreasing(LOAD1221(+(i118[3], -1), +(i119[3], -1), i84[3])), ≥)∧[(2)bni_35] = 0∧[(-2)bni_35 + (-1)Bound*bni_35] + [(-2)bni_35]i84[2] + [(-1)bni_35]i119[2] ≥ 0∧0 = 0∧[1 + (-1)bso_36] ≥ 0)

  • LOAD1221(i118, i119, i84) → COND_LOAD12211(<=(i119, i84), i118, i119, i84)
    • (i84[4] ≥ 0∧i119[4] ≥ 0 ⇒ (UIncreasing(COND_LOAD12211(<=(i119[4], i84[4]), i118[4], i119[4], i84[4])), ≥)∧[(2)bni_37] = 0∧[(-1)bni_37 + (-1)Bound*bni_37] + [(-2)bni_37]i119[4] + [(-1)bni_37]i84[4] ≥ 0∧0 = 0∧[(-1)bso_38] ≥ 0)
    • (i84[4] ≥ 0∧i119[4] ≥ 0 ⇒ (UIncreasing(COND_LOAD12211(<=(i119[4], i84[4]), i118[4], i119[4], i84[4])), ≥)∧[(2)bni_37] = 0∧[(-1)bni_37 + (-1)Bound*bni_37] + [(2)bni_37]i119[4] + [(-1)bni_37]i84[4] ≥ 0∧0 = 0∧[(-1)bso_38] ≥ 0)

  • COND_LOAD12211(TRUE, i118, i119, i84) → LOAD1146(i118, i119, i84)
    • ((UIncreasing(LOAD1146(i118[5], i119[5], i84[5])), ≥)∧0 = 0∧0 = 0∧[(-1)bso_40] ≥ 0)




The constraints for P> respective Pbound are constructed from P≥ where we just replace every occurence of "t ≥ s" in P≥ by "t > s" respective "t ≥ c". Here c stands for the fresh constant used for Pbound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation over integers[POLO]:

POL(TRUE) = 0   
POL(FALSE) = [3]   
POL(LOAD1146(x1, x2, x3)) = [-1] + [-1]x3 + [-1]x2 + [2]x1   
POL(COND_LOAD1146(x1, x2, x3)) = [-1] + [-1]x3 + x2   
POL(&&(x1, x2)) = [-1]   
POL(>=(x1, x2)) = [-1]   
POL(0) = 0   
POL(>(x1, x2)) = [-1]   
POL(LOAD1221(x1, x2, x3)) = [-1] + [-1]x3 + [-1]x2 + [2]x1   
POL(COND_LOAD1221(x1, x2, x3, x4)) = [-1] + [-1]x4 + [-1]x3 + [2]x2   
POL(+(x1, x2)) = x1 + x2   
POL(-1) = [-1]   
POL(COND_LOAD12211(x1, x2, x3, x4)) = [-1] + [-1]x4 + [-1]x3 + [2]x2   
POL(<=(x1, x2)) = [-1]   

The following pairs are in P>:

COND_LOAD1221(TRUE, i118[3], i119[3], i84[3]) → LOAD1221(+(i118[3], -1), +(i119[3], -1), i84[3])

The following pairs are in Pbound:

LOAD1146(i112[0], i112[0], i84[0]) → COND_LOAD1146(&&(>=(i84[0], 0), >(i112[0], i84[0])), i112[0], i84[0])

The following pairs are in P≥:

LOAD1146(i112[0], i112[0], i84[0]) → COND_LOAD1146(&&(>=(i84[0], 0), >(i112[0], i84[0])), i112[0], i84[0])
COND_LOAD1146(TRUE, i112[1], i84[1]) → LOAD1221(i112[1], i112[1], i84[1])
LOAD1221(i118[2], i119[2], i84[2]) → COND_LOAD1221(&&(>=(i84[2], 0), >(i119[2], i84[2])), i118[2], i119[2], i84[2])
LOAD1221(i118[4], i119[4], i84[4]) → COND_LOAD12211(<=(i119[4], i84[4]), i118[4], i119[4], i84[4])
COND_LOAD12211(TRUE, i118[5], i119[5], i84[5]) → LOAD1146(i118[5], i119[5], i84[5])

At least the following rules have been oriented under context sensitive arithmetic replacement:

TRUE1 → &&(TRUE, TRUE)1
FALSE1 → &&(TRUE, FALSE)1
FALSE1 → &&(FALSE, TRUE)1
FALSE1 → &&(FALSE, FALSE)1

(12) Complex Obligation (AND)

(13) Obligation:

IDP problem:
The following function symbols are pre-defined:
!=~Neq: (Integer, Integer) -> Boolean
*~Mul: (Integer, Integer) -> Integer
>=~Ge: (Integer, Integer) -> Boolean
-1~UnaryMinus: (Integer) -> Integer
|~Bwor: (Integer, Integer) -> Integer
/~Div: (Integer, Integer) -> Integer
=~Eq: (Integer, Integer) -> Boolean
~Bwxor: (Integer, Integer) -> Integer
||~Lor: (Boolean, Boolean) -> Boolean
!~Lnot: (Boolean) -> Boolean
<~Lt: (Integer, Integer) -> Boolean
-~Sub: (Integer, Integer) -> Integer
<=~Le: (Integer, Integer) -> Boolean
>~Gt: (Integer, Integer) -> Boolean
~~Bwnot: (Integer) -> Integer
%~Mod: (Integer, Integer) -> Integer
&~Bwand: (Integer, Integer) -> Integer
+~Add: (Integer, Integer) -> Integer
&&~Land: (Boolean, Boolean) -> Boolean


The following domains are used:

Boolean, Integer


R is empty.

The integer pair graph contains the following rules and edges:
(0): LOAD1146(i112[0], i112[0], i84[0]) → COND_LOAD1146(i84[0] >= 0 && i112[0] > i84[0], i112[0], i84[0])
(1): COND_LOAD1146(TRUE, i112[1], i84[1]) → LOAD1221(i112[1], i112[1], i84[1])
(2): LOAD1221(i118[2], i119[2], i84[2]) → COND_LOAD1221(i84[2] >= 0 && i119[2] > i84[2], i118[2], i119[2], i84[2])
(4): LOAD1221(i118[4], i119[4], i84[4]) → COND_LOAD12211(i119[4] <= i84[4], i118[4], i119[4], i84[4])
(5): COND_LOAD12211(TRUE, i118[5], i119[5], i84[5]) → LOAD1146(i118[5], i119[5], i84[5])

(5) -> (0), if ((i118[5] →* i112[0])∧(i84[5] →* i84[0])∧(i119[5] →* i112[0]))


(0) -> (1), if ((i112[0] →* i112[1])∧(i84[0] >= 0 && i112[0] > i84[0] →* TRUE)∧(i84[0] →* i84[1]))


(1) -> (2), if ((i112[1] →* i118[2])∧(i112[1] →* i119[2])∧(i84[1] →* i84[2]))


(1) -> (4), if ((i112[1] →* i119[4])∧(i112[1] →* i118[4])∧(i84[1] →* i84[4]))


(4) -> (5), if ((i119[4] →* i119[5])∧(i84[4] →* i84[5])∧(i118[4] →* i118[5])∧(i119[4] <= i84[4] →* TRUE))



The set Q consists of the following terms:
Load1146(x0, x0, x1)
Cond_Load1146(TRUE, x0, x1)
Load1221(x0, x1, x2)
Cond_Load1221(TRUE, x0, x1, x2)
Cond_Load12211(TRUE, x0, x1, x2)

(14) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(15) Obligation:

IDP problem:
The following function symbols are pre-defined:
!=~Neq: (Integer, Integer) -> Boolean
*~Mul: (Integer, Integer) -> Integer
>=~Ge: (Integer, Integer) -> Boolean
-1~UnaryMinus: (Integer) -> Integer
|~Bwor: (Integer, Integer) -> Integer
/~Div: (Integer, Integer) -> Integer
=~Eq: (Integer, Integer) -> Boolean
~Bwxor: (Integer, Integer) -> Integer
||~Lor: (Boolean, Boolean) -> Boolean
!~Lnot: (Boolean) -> Boolean
<~Lt: (Integer, Integer) -> Boolean
-~Sub: (Integer, Integer) -> Integer
<=~Le: (Integer, Integer) -> Boolean
>~Gt: (Integer, Integer) -> Boolean
~~Bwnot: (Integer) -> Integer
%~Mod: (Integer, Integer) -> Integer
&~Bwand: (Integer, Integer) -> Integer
+~Add: (Integer, Integer) -> Integer
&&~Land: (Boolean, Boolean) -> Boolean


The following domains are used:

Integer, Boolean


R is empty.

The integer pair graph contains the following rules and edges:
(5): COND_LOAD12211(TRUE, i118[5], i119[5], i84[5]) → LOAD1146(i118[5], i119[5], i84[5])
(4): LOAD1221(i118[4], i119[4], i84[4]) → COND_LOAD12211(i119[4] <= i84[4], i118[4], i119[4], i84[4])
(1): COND_LOAD1146(TRUE, i112[1], i84[1]) → LOAD1221(i112[1], i112[1], i84[1])
(0): LOAD1146(i112[0], i112[0], i84[0]) → COND_LOAD1146(i84[0] >= 0 && i112[0] > i84[0], i112[0], i84[0])

(5) -> (0), if ((i118[5] →* i112[0])∧(i84[5] →* i84[0])∧(i119[5] →* i112[0]))


(0) -> (1), if ((i112[0] →* i112[1])∧(i84[0] >= 0 && i112[0] > i84[0] →* TRUE)∧(i84[0] →* i84[1]))


(1) -> (4), if ((i112[1] →* i119[4])∧(i112[1] →* i118[4])∧(i84[1] →* i84[4]))


(4) -> (5), if ((i119[4] →* i119[5])∧(i84[4] →* i84[5])∧(i118[4] →* i118[5])∧(i119[4] <= i84[4] →* TRUE))



The set Q consists of the following terms:
Load1146(x0, x0, x1)
Cond_Load1146(TRUE, x0, x1)
Load1221(x0, x1, x2)
Cond_Load1221(TRUE, x0, x1, x2)
Cond_Load12211(TRUE, x0, x1, x2)

(16) IDPNonInfProof (SOUND transformation)

The constraints were generated the following way:
The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that final constraints are written in bold face.


For Pair COND_LOAD12211(TRUE, i118[5], i119[5], i84[5]) → LOAD1146(i118[5], i119[5], i84[5]) the following chains were created:
  • We consider the chain LOAD1221(i118[4], i119[4], i84[4]) → COND_LOAD12211(<=(i119[4], i84[4]), i118[4], i119[4], i84[4]), COND_LOAD12211(TRUE, i118[5], i119[5], i84[5]) → LOAD1146(i118[5], i119[5], i84[5]), LOAD1146(i112[0], i112[0], i84[0]) → COND_LOAD1146(&&(>=(i84[0], 0), >(i112[0], i84[0])), i112[0], i84[0]) which results in the following constraint:

    (1)    (i119[4]=i119[5]∧i84[4]=i84[5]∧i118[4]=i118[5]∧<=(i119[4], i84[4])=TRUE∧i118[5]=i112[0]∧i84[5]=i84[0]∧i119[5]=i112[0] ⇒ COND_LOAD12211(TRUE, i118[5], i119[5], i84[5])≥NonInfC∧COND_LOAD12211(TRUE, i118[5], i119[5], i84[5])≥LOAD1146(i118[5], i119[5], i84[5])∧(UIncreasing(LOAD1146(i118[5], i119[5], i84[5])), ≥))



    We simplified constraint (1) using rules (III), (IV) which results in the following new constraint:

    (2)    (<=(i119[4], i84[4])=TRUE ⇒ COND_LOAD12211(TRUE, i119[4], i119[4], i84[4])≥NonInfC∧COND_LOAD12211(TRUE, i119[4], i119[4], i84[4])≥LOAD1146(i119[4], i119[4], i84[4])∧(UIncreasing(LOAD1146(i118[5], i119[5], i84[5])), ≥))



    We simplified constraint (2) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (3)    (i84[4] + [-1]i119[4] ≥ 0 ⇒ (UIncreasing(LOAD1146(i118[5], i119[5], i84[5])), ≥)∧[(-1)bni_24 + (-1)Bound*bni_24] + [(-1)bni_24]i84[4] + [bni_24]i119[4] ≥ 0∧[(-1)bso_25] ≥ 0)



    We simplified constraint (3) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (4)    (i84[4] + [-1]i119[4] ≥ 0 ⇒ (UIncreasing(LOAD1146(i118[5], i119[5], i84[5])), ≥)∧[(-1)bni_24 + (-1)Bound*bni_24] + [(-1)bni_24]i84[4] + [bni_24]i119[4] ≥ 0∧[(-1)bso_25] ≥ 0)



    We simplified constraint (4) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (5)    (i84[4] + [-1]i119[4] ≥ 0 ⇒ (UIncreasing(LOAD1146(i118[5], i119[5], i84[5])), ≥)∧[(-1)bni_24 + (-1)Bound*bni_24] + [(-1)bni_24]i84[4] + [bni_24]i119[4] ≥ 0∧[(-1)bso_25] ≥ 0)



    We simplified constraint (5) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (6)    (i84[4] ≥ 0 ⇒ (UIncreasing(LOAD1146(i118[5], i119[5], i84[5])), ≥)∧[(-1)bni_24 + (-1)Bound*bni_24] + [(-1)bni_24]i84[4] ≥ 0∧[(-1)bso_25] ≥ 0)



    We simplified constraint (6) using rule (IDP_SMT_SPLIT) which results in the following new constraints:

    (7)    (i84[4] ≥ 0∧i119[4] ≥ 0 ⇒ (UIncreasing(LOAD1146(i118[5], i119[5], i84[5])), ≥)∧[(-1)bni_24 + (-1)Bound*bni_24] + [(-1)bni_24]i84[4] ≥ 0∧[(-1)bso_25] ≥ 0)


    (8)    (i84[4] ≥ 0∧i119[4] ≥ 0 ⇒ (UIncreasing(LOAD1146(i118[5], i119[5], i84[5])), ≥)∧[(-1)bni_24 + (-1)Bound*bni_24] + [(-1)bni_24]i84[4] ≥ 0∧[(-1)bso_25] ≥ 0)







For Pair LOAD1221(i118[4], i119[4], i84[4]) → COND_LOAD12211(<=(i119[4], i84[4]), i118[4], i119[4], i84[4]) the following chains were created:
  • We consider the chain COND_LOAD1146(TRUE, i112[1], i84[1]) → LOAD1221(i112[1], i112[1], i84[1]), LOAD1221(i118[4], i119[4], i84[4]) → COND_LOAD12211(<=(i119[4], i84[4]), i118[4], i119[4], i84[4]), COND_LOAD12211(TRUE, i118[5], i119[5], i84[5]) → LOAD1146(i118[5], i119[5], i84[5]) which results in the following constraint:

    (9)    (i112[1]=i119[4]∧i112[1]=i118[4]∧i84[1]=i84[4]∧i119[4]=i119[5]∧i84[4]=i84[5]∧i118[4]=i118[5]∧<=(i119[4], i84[4])=TRUE ⇒ LOAD1221(i118[4], i119[4], i84[4])≥NonInfC∧LOAD1221(i118[4], i119[4], i84[4])≥COND_LOAD12211(<=(i119[4], i84[4]), i118[4], i119[4], i84[4])∧(UIncreasing(COND_LOAD12211(<=(i119[4], i84[4]), i118[4], i119[4], i84[4])), ≥))



    We simplified constraint (9) using rules (III), (IV) which results in the following new constraint:

    (10)    (<=(i119[4], i84[4])=TRUE ⇒ LOAD1221(i119[4], i119[4], i84[4])≥NonInfC∧LOAD1221(i119[4], i119[4], i84[4])≥COND_LOAD12211(<=(i119[4], i84[4]), i119[4], i119[4], i84[4])∧(UIncreasing(COND_LOAD12211(<=(i119[4], i84[4]), i118[4], i119[4], i84[4])), ≥))



    We simplified constraint (10) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (11)    (i84[4] + [-1]i119[4] ≥ 0 ⇒ (UIncreasing(COND_LOAD12211(<=(i119[4], i84[4]), i118[4], i119[4], i84[4])), ≥)∧[(-1)bni_26 + (-1)Bound*bni_26] + [bni_26]i84[4] + [(-1)bni_26]i119[4] ≥ 0∧[(-1)bso_27] + [2]i84[4] + [-2]i119[4] ≥ 0)



    We simplified constraint (11) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (12)    (i84[4] + [-1]i119[4] ≥ 0 ⇒ (UIncreasing(COND_LOAD12211(<=(i119[4], i84[4]), i118[4], i119[4], i84[4])), ≥)∧[(-1)bni_26 + (-1)Bound*bni_26] + [bni_26]i84[4] + [(-1)bni_26]i119[4] ≥ 0∧[(-1)bso_27] + [2]i84[4] + [-2]i119[4] ≥ 0)



    We simplified constraint (12) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (13)    (i84[4] + [-1]i119[4] ≥ 0 ⇒ (UIncreasing(COND_LOAD12211(<=(i119[4], i84[4]), i118[4], i119[4], i84[4])), ≥)∧[(-1)bni_26 + (-1)Bound*bni_26] + [bni_26]i84[4] + [(-1)bni_26]i119[4] ≥ 0∧[(-1)bso_27] + [2]i84[4] + [-2]i119[4] ≥ 0)



    We simplified constraint (13) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (14)    (i84[4] ≥ 0 ⇒ (UIncreasing(COND_LOAD12211(<=(i119[4], i84[4]), i118[4], i119[4], i84[4])), ≥)∧[(-1)bni_26 + (-1)Bound*bni_26] + [bni_26]i84[4] ≥ 0∧[(-1)bso_27] + [2]i84[4] ≥ 0)



    We simplified constraint (14) using rule (IDP_SMT_SPLIT) which results in the following new constraints:

    (15)    (i84[4] ≥ 0∧i119[4] ≥ 0 ⇒ (UIncreasing(COND_LOAD12211(<=(i119[4], i84[4]), i118[4], i119[4], i84[4])), ≥)∧[(-1)bni_26 + (-1)Bound*bni_26] + [bni_26]i84[4] ≥ 0∧[(-1)bso_27] + [2]i84[4] ≥ 0)


    (16)    (i84[4] ≥ 0∧i119[4] ≥ 0 ⇒ (UIncreasing(COND_LOAD12211(<=(i119[4], i84[4]), i118[4], i119[4], i84[4])), ≥)∧[(-1)bni_26 + (-1)Bound*bni_26] + [bni_26]i84[4] ≥ 0∧[(-1)bso_27] + [2]i84[4] ≥ 0)







For Pair COND_LOAD1146(TRUE, i112[1], i84[1]) → LOAD1221(i112[1], i112[1], i84[1]) the following chains were created:
  • We consider the chain LOAD1146(i112[0], i112[0], i84[0]) → COND_LOAD1146(&&(>=(i84[0], 0), >(i112[0], i84[0])), i112[0], i84[0]), COND_LOAD1146(TRUE, i112[1], i84[1]) → LOAD1221(i112[1], i112[1], i84[1]), LOAD1221(i118[4], i119[4], i84[4]) → COND_LOAD12211(<=(i119[4], i84[4]), i118[4], i119[4], i84[4]) which results in the following constraint:

    (17)    (i112[0]=i112[1]∧&&(>=(i84[0], 0), >(i112[0], i84[0]))=TRUE∧i84[0]=i84[1]∧i112[1]=i119[4]∧i112[1]=i118[4]∧i84[1]=i84[4] ⇒ COND_LOAD1146(TRUE, i112[1], i84[1])≥NonInfC∧COND_LOAD1146(TRUE, i112[1], i84[1])≥LOAD1221(i112[1], i112[1], i84[1])∧(UIncreasing(LOAD1221(i112[1], i112[1], i84[1])), ≥))



    We simplified constraint (17) using rules (III), (IV), (IDP_BOOLEAN) which results in the following new constraint:

    (18)    (>=(i84[0], 0)=TRUE∧>(i112[0], i84[0])=TRUE ⇒ COND_LOAD1146(TRUE, i112[0], i84[0])≥NonInfC∧COND_LOAD1146(TRUE, i112[0], i84[0])≥LOAD1221(i112[0], i112[0], i84[0])∧(UIncreasing(LOAD1221(i112[1], i112[1], i84[1])), ≥))



    We simplified constraint (18) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (19)    (i84[0] ≥ 0∧i112[0] + [-1] + [-1]i84[0] ≥ 0 ⇒ (UIncreasing(LOAD1221(i112[1], i112[1], i84[1])), ≥)∧[(-1)bni_28 + (-1)Bound*bni_28] + [bni_28]i84[0] + [(-1)bni_28]i112[0] ≥ 0∧[(-1)bso_29] ≥ 0)



    We simplified constraint (19) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (20)    (i84[0] ≥ 0∧i112[0] + [-1] + [-1]i84[0] ≥ 0 ⇒ (UIncreasing(LOAD1221(i112[1], i112[1], i84[1])), ≥)∧[(-1)bni_28 + (-1)Bound*bni_28] + [bni_28]i84[0] + [(-1)bni_28]i112[0] ≥ 0∧[(-1)bso_29] ≥ 0)



    We simplified constraint (20) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (21)    (i84[0] ≥ 0∧i112[0] + [-1] + [-1]i84[0] ≥ 0 ⇒ (UIncreasing(LOAD1221(i112[1], i112[1], i84[1])), ≥)∧[(-1)bni_28 + (-1)Bound*bni_28] + [bni_28]i84[0] + [(-1)bni_28]i112[0] ≥ 0∧[(-1)bso_29] ≥ 0)



    We simplified constraint (21) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (22)    (i84[0] ≥ 0∧i112[0] ≥ 0 ⇒ (UIncreasing(LOAD1221(i112[1], i112[1], i84[1])), ≥)∧[(-2)bni_28 + (-1)Bound*bni_28] + [(-1)bni_28]i112[0] ≥ 0∧[(-1)bso_29] ≥ 0)







For Pair LOAD1146(i112[0], i112[0], i84[0]) → COND_LOAD1146(&&(>=(i84[0], 0), >(i112[0], i84[0])), i112[0], i84[0]) the following chains were created:
  • We consider the chain COND_LOAD12211(TRUE, i118[5], i119[5], i84[5]) → LOAD1146(i118[5], i119[5], i84[5]), LOAD1146(i112[0], i112[0], i84[0]) → COND_LOAD1146(&&(>=(i84[0], 0), >(i112[0], i84[0])), i112[0], i84[0]), COND_LOAD1146(TRUE, i112[1], i84[1]) → LOAD1221(i112[1], i112[1], i84[1]) which results in the following constraint:

    (23)    (i118[5]=i112[0]∧i84[5]=i84[0]∧i119[5]=i112[0]∧i112[0]=i112[1]∧&&(>=(i84[0], 0), >(i112[0], i84[0]))=TRUE∧i84[0]=i84[1] ⇒ LOAD1146(i112[0], i112[0], i84[0])≥NonInfC∧LOAD1146(i112[0], i112[0], i84[0])≥COND_LOAD1146(&&(>=(i84[0], 0), >(i112[0], i84[0])), i112[0], i84[0])∧(UIncreasing(COND_LOAD1146(&&(>=(i84[0], 0), >(i112[0], i84[0])), i112[0], i84[0])), ≥))



    We simplified constraint (23) using rules (III), (IV), (IDP_BOOLEAN) which results in the following new constraint:

    (24)    (>=(i84[0], 0)=TRUE∧>(i112[0], i84[0])=TRUE ⇒ LOAD1146(i112[0], i112[0], i84[0])≥NonInfC∧LOAD1146(i112[0], i112[0], i84[0])≥COND_LOAD1146(&&(>=(i84[0], 0), >(i112[0], i84[0])), i112[0], i84[0])∧(UIncreasing(COND_LOAD1146(&&(>=(i84[0], 0), >(i112[0], i84[0])), i112[0], i84[0])), ≥))



    We simplified constraint (24) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (25)    (i84[0] ≥ 0∧i112[0] + [-1] + [-1]i84[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1146(&&(>=(i84[0], 0), >(i112[0], i84[0])), i112[0], i84[0])), ≥)∧[(-1)bni_30 + (-1)Bound*bni_30] + [(-1)bni_30]i84[0] + [bni_30]i112[0] ≥ 0∧[-1 + (-1)bso_31] + [-2]i84[0] + [2]i112[0] ≥ 0)



    We simplified constraint (25) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (26)    (i84[0] ≥ 0∧i112[0] + [-1] + [-1]i84[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1146(&&(>=(i84[0], 0), >(i112[0], i84[0])), i112[0], i84[0])), ≥)∧[(-1)bni_30 + (-1)Bound*bni_30] + [(-1)bni_30]i84[0] + [bni_30]i112[0] ≥ 0∧[-1 + (-1)bso_31] + [-2]i84[0] + [2]i112[0] ≥ 0)



    We simplified constraint (26) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (27)    (i84[0] ≥ 0∧i112[0] + [-1] + [-1]i84[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1146(&&(>=(i84[0], 0), >(i112[0], i84[0])), i112[0], i84[0])), ≥)∧[(-1)bni_30 + (-1)Bound*bni_30] + [(-1)bni_30]i84[0] + [bni_30]i112[0] ≥ 0∧[-1 + (-1)bso_31] + [-2]i84[0] + [2]i112[0] ≥ 0)



    We simplified constraint (27) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (28)    (i84[0] ≥ 0∧i112[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1146(&&(>=(i84[0], 0), >(i112[0], i84[0])), i112[0], i84[0])), ≥)∧[(-1)Bound*bni_30] + [bni_30]i112[0] ≥ 0∧[1 + (-1)bso_31] + [2]i112[0] ≥ 0)







To summarize, we get the following constraints P≥ for the following pairs.
  • COND_LOAD12211(TRUE, i118[5], i119[5], i84[5]) → LOAD1146(i118[5], i119[5], i84[5])
    • (i84[4] ≥ 0∧i119[4] ≥ 0 ⇒ (UIncreasing(LOAD1146(i118[5], i119[5], i84[5])), ≥)∧[(-1)bni_24 + (-1)Bound*bni_24] + [(-1)bni_24]i84[4] ≥ 0∧[(-1)bso_25] ≥ 0)
    • (i84[4] ≥ 0∧i119[4] ≥ 0 ⇒ (UIncreasing(LOAD1146(i118[5], i119[5], i84[5])), ≥)∧[(-1)bni_24 + (-1)Bound*bni_24] + [(-1)bni_24]i84[4] ≥ 0∧[(-1)bso_25] ≥ 0)

  • LOAD1221(i118[4], i119[4], i84[4]) → COND_LOAD12211(<=(i119[4], i84[4]), i118[4], i119[4], i84[4])
    • (i84[4] ≥ 0∧i119[4] ≥ 0 ⇒ (UIncreasing(COND_LOAD12211(<=(i119[4], i84[4]), i118[4], i119[4], i84[4])), ≥)∧[(-1)bni_26 + (-1)Bound*bni_26] + [bni_26]i84[4] ≥ 0∧[(-1)bso_27] + [2]i84[4] ≥ 0)
    • (i84[4] ≥ 0∧i119[4] ≥ 0 ⇒ (UIncreasing(COND_LOAD12211(<=(i119[4], i84[4]), i118[4], i119[4], i84[4])), ≥)∧[(-1)bni_26 + (-1)Bound*bni_26] + [bni_26]i84[4] ≥ 0∧[(-1)bso_27] + [2]i84[4] ≥ 0)

  • COND_LOAD1146(TRUE, i112[1], i84[1]) → LOAD1221(i112[1], i112[1], i84[1])
    • (i84[0] ≥ 0∧i112[0] ≥ 0 ⇒ (UIncreasing(LOAD1221(i112[1], i112[1], i84[1])), ≥)∧[(-2)bni_28 + (-1)Bound*bni_28] + [(-1)bni_28]i112[0] ≥ 0∧[(-1)bso_29] ≥ 0)

  • LOAD1146(i112[0], i112[0], i84[0]) → COND_LOAD1146(&&(>=(i84[0], 0), >(i112[0], i84[0])), i112[0], i84[0])
    • (i84[0] ≥ 0∧i112[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1146(&&(>=(i84[0], 0), >(i112[0], i84[0])), i112[0], i84[0])), ≥)∧[(-1)Bound*bni_30] + [bni_30]i112[0] ≥ 0∧[1 + (-1)bso_31] + [2]i112[0] ≥ 0)




The constraints for P> respective Pbound are constructed from P≥ where we just replace every occurence of "t ≥ s" in P≥ by "t > s" respective "t ≥ c". Here c stands for the fresh constant used for Pbound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation over integers[POLO]:

POL(TRUE) = 0   
POL(FALSE) = 0   
POL(COND_LOAD12211(x1, x2, x3, x4)) = [-1] + [-1]x4 + [-1]x3 + [2]x2   
POL(LOAD1146(x1, x2, x3)) = [-1] + [-1]x3 + [-1]x2 + [2]x1   
POL(LOAD1221(x1, x2, x3)) = [-1] + x3 + [-1]x2   
POL(<=(x1, x2)) = [-1]   
POL(COND_LOAD1146(x1, x2, x3)) = [-1] + x3 + [-1]x2 + [-1]x1   
POL(&&(x1, x2)) = [-1]   
POL(>=(x1, x2)) = [-1]   
POL(0) = 0   
POL(>(x1, x2)) = [-1]   

The following pairs are in P>:

LOAD1146(i112[0], i112[0], i84[0]) → COND_LOAD1146(&&(>=(i84[0], 0), >(i112[0], i84[0])), i112[0], i84[0])

The following pairs are in Pbound:

LOAD1221(i118[4], i119[4], i84[4]) → COND_LOAD12211(<=(i119[4], i84[4]), i118[4], i119[4], i84[4])
LOAD1146(i112[0], i112[0], i84[0]) → COND_LOAD1146(&&(>=(i84[0], 0), >(i112[0], i84[0])), i112[0], i84[0])

The following pairs are in P≥:

COND_LOAD12211(TRUE, i118[5], i119[5], i84[5]) → LOAD1146(i118[5], i119[5], i84[5])
LOAD1221(i118[4], i119[4], i84[4]) → COND_LOAD12211(<=(i119[4], i84[4]), i118[4], i119[4], i84[4])
COND_LOAD1146(TRUE, i112[1], i84[1]) → LOAD1221(i112[1], i112[1], i84[1])

At least the following rules have been oriented under context sensitive arithmetic replacement:

TRUE1 → &&(TRUE, TRUE)1
FALSE1 → &&(TRUE, FALSE)1
FALSE1 → &&(FALSE, TRUE)1
FALSE1 → &&(FALSE, FALSE)1

(17) Complex Obligation (AND)

(18) Obligation:

IDP problem:
The following function symbols are pre-defined:
!=~Neq: (Integer, Integer) -> Boolean
*~Mul: (Integer, Integer) -> Integer
>=~Ge: (Integer, Integer) -> Boolean
-1~UnaryMinus: (Integer) -> Integer
|~Bwor: (Integer, Integer) -> Integer
/~Div: (Integer, Integer) -> Integer
=~Eq: (Integer, Integer) -> Boolean
~Bwxor: (Integer, Integer) -> Integer
||~Lor: (Boolean, Boolean) -> Boolean
!~Lnot: (Boolean) -> Boolean
<~Lt: (Integer, Integer) -> Boolean
-~Sub: (Integer, Integer) -> Integer
<=~Le: (Integer, Integer) -> Boolean
>~Gt: (Integer, Integer) -> Boolean
~~Bwnot: (Integer) -> Integer
%~Mod: (Integer, Integer) -> Integer
&~Bwand: (Integer, Integer) -> Integer
+~Add: (Integer, Integer) -> Integer
&&~Land: (Boolean, Boolean) -> Boolean


The following domains are used:

Integer


R is empty.

The integer pair graph contains the following rules and edges:
(5): COND_LOAD12211(TRUE, i118[5], i119[5], i84[5]) → LOAD1146(i118[5], i119[5], i84[5])
(4): LOAD1221(i118[4], i119[4], i84[4]) → COND_LOAD12211(i119[4] <= i84[4], i118[4], i119[4], i84[4])
(1): COND_LOAD1146(TRUE, i112[1], i84[1]) → LOAD1221(i112[1], i112[1], i84[1])

(1) -> (4), if ((i112[1] →* i119[4])∧(i112[1] →* i118[4])∧(i84[1] →* i84[4]))


(4) -> (5), if ((i119[4] →* i119[5])∧(i84[4] →* i84[5])∧(i118[4] →* i118[5])∧(i119[4] <= i84[4] →* TRUE))



The set Q consists of the following terms:
Load1146(x0, x0, x1)
Cond_Load1146(TRUE, x0, x1)
Load1221(x0, x1, x2)
Cond_Load1221(TRUE, x0, x1, x2)
Cond_Load12211(TRUE, x0, x1, x2)

(19) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 3 less nodes.

(20) TRUE

(21) Obligation:

IDP problem:
The following function symbols are pre-defined:
!=~Neq: (Integer, Integer) -> Boolean
*~Mul: (Integer, Integer) -> Integer
>=~Ge: (Integer, Integer) -> Boolean
-1~UnaryMinus: (Integer) -> Integer
|~Bwor: (Integer, Integer) -> Integer
/~Div: (Integer, Integer) -> Integer
=~Eq: (Integer, Integer) -> Boolean
~Bwxor: (Integer, Integer) -> Integer
||~Lor: (Boolean, Boolean) -> Boolean
!~Lnot: (Boolean) -> Boolean
<~Lt: (Integer, Integer) -> Boolean
-~Sub: (Integer, Integer) -> Integer
<=~Le: (Integer, Integer) -> Boolean
>~Gt: (Integer, Integer) -> Boolean
~~Bwnot: (Integer) -> Integer
%~Mod: (Integer, Integer) -> Integer
&~Bwand: (Integer, Integer) -> Integer
+~Add: (Integer, Integer) -> Integer
&&~Land: (Boolean, Boolean) -> Boolean


The following domains are used:
none


R is empty.

The integer pair graph contains the following rules and edges:
(5): COND_LOAD12211(TRUE, i118[5], i119[5], i84[5]) → LOAD1146(i118[5], i119[5], i84[5])
(1): COND_LOAD1146(TRUE, i112[1], i84[1]) → LOAD1221(i112[1], i112[1], i84[1])


The set Q consists of the following terms:
Load1146(x0, x0, x1)
Cond_Load1146(TRUE, x0, x1)
Load1221(x0, x1, x2)
Cond_Load1221(TRUE, x0, x1, x2)
Cond_Load12211(TRUE, x0, x1, x2)

(22) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 2 less nodes.

(23) TRUE

(24) Obligation:

IDP problem:
The following function symbols are pre-defined:
!=~Neq: (Integer, Integer) -> Boolean
*~Mul: (Integer, Integer) -> Integer
>=~Ge: (Integer, Integer) -> Boolean
-1~UnaryMinus: (Integer) -> Integer
|~Bwor: (Integer, Integer) -> Integer
/~Div: (Integer, Integer) -> Integer
=~Eq: (Integer, Integer) -> Boolean
~Bwxor: (Integer, Integer) -> Integer
||~Lor: (Boolean, Boolean) -> Boolean
!~Lnot: (Boolean) -> Boolean
<~Lt: (Integer, Integer) -> Boolean
-~Sub: (Integer, Integer) -> Integer
<=~Le: (Integer, Integer) -> Boolean
>~Gt: (Integer, Integer) -> Boolean
~~Bwnot: (Integer) -> Integer
%~Mod: (Integer, Integer) -> Integer
&~Bwand: (Integer, Integer) -> Integer
+~Add: (Integer, Integer) -> Integer
&&~Land: (Boolean, Boolean) -> Boolean


The following domains are used:

Boolean, Integer


R is empty.

The integer pair graph contains the following rules and edges:
(1): COND_LOAD1146(TRUE, i112[1], i84[1]) → LOAD1221(i112[1], i112[1], i84[1])
(2): LOAD1221(i118[2], i119[2], i84[2]) → COND_LOAD1221(i84[2] >= 0 && i119[2] > i84[2], i118[2], i119[2], i84[2])
(3): COND_LOAD1221(TRUE, i118[3], i119[3], i84[3]) → LOAD1221(i118[3] + -1, i119[3] + -1, i84[3])
(4): LOAD1221(i118[4], i119[4], i84[4]) → COND_LOAD12211(i119[4] <= i84[4], i118[4], i119[4], i84[4])
(5): COND_LOAD12211(TRUE, i118[5], i119[5], i84[5]) → LOAD1146(i118[5], i119[5], i84[5])

(1) -> (2), if ((i112[1] →* i118[2])∧(i112[1] →* i119[2])∧(i84[1] →* i84[2]))


(3) -> (2), if ((i119[3] + -1 →* i119[2])∧(i118[3] + -1 →* i118[2])∧(i84[3] →* i84[2]))


(2) -> (3), if ((i84[2] >= 0 && i119[2] > i84[2] →* TRUE)∧(i119[2] →* i119[3])∧(i84[2] →* i84[3])∧(i118[2] →* i118[3]))


(1) -> (4), if ((i112[1] →* i119[4])∧(i112[1] →* i118[4])∧(i84[1] →* i84[4]))


(3) -> (4), if ((i84[3] →* i84[4])∧(i119[3] + -1 →* i119[4])∧(i118[3] + -1 →* i118[4]))


(4) -> (5), if ((i119[4] →* i119[5])∧(i84[4] →* i84[5])∧(i118[4] →* i118[5])∧(i119[4] <= i84[4] →* TRUE))



The set Q consists of the following terms:
Load1146(x0, x0, x1)
Cond_Load1146(TRUE, x0, x1)
Load1221(x0, x1, x2)
Cond_Load1221(TRUE, x0, x1, x2)
Cond_Load12211(TRUE, x0, x1, x2)

(25) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 3 less nodes.

(26) Obligation:

IDP problem:
The following function symbols are pre-defined:
!=~Neq: (Integer, Integer) -> Boolean
*~Mul: (Integer, Integer) -> Integer
>=~Ge: (Integer, Integer) -> Boolean
-1~UnaryMinus: (Integer) -> Integer
|~Bwor: (Integer, Integer) -> Integer
/~Div: (Integer, Integer) -> Integer
=~Eq: (Integer, Integer) -> Boolean
~Bwxor: (Integer, Integer) -> Integer
||~Lor: (Boolean, Boolean) -> Boolean
!~Lnot: (Boolean) -> Boolean
<~Lt: (Integer, Integer) -> Boolean
-~Sub: (Integer, Integer) -> Integer
<=~Le: (Integer, Integer) -> Boolean
>~Gt: (Integer, Integer) -> Boolean
~~Bwnot: (Integer) -> Integer
%~Mod: (Integer, Integer) -> Integer
&~Bwand: (Integer, Integer) -> Integer
+~Add: (Integer, Integer) -> Integer
&&~Land: (Boolean, Boolean) -> Boolean


The following domains are used:

Integer, Boolean


R is empty.

The integer pair graph contains the following rules and edges:
(3): COND_LOAD1221(TRUE, i118[3], i119[3], i84[3]) → LOAD1221(i118[3] + -1, i119[3] + -1, i84[3])
(2): LOAD1221(i118[2], i119[2], i84[2]) → COND_LOAD1221(i84[2] >= 0 && i119[2] > i84[2], i118[2], i119[2], i84[2])

(3) -> (2), if ((i119[3] + -1 →* i119[2])∧(i118[3] + -1 →* i118[2])∧(i84[3] →* i84[2]))


(2) -> (3), if ((i84[2] >= 0 && i119[2] > i84[2] →* TRUE)∧(i119[2] →* i119[3])∧(i84[2] →* i84[3])∧(i118[2] →* i118[3]))



The set Q consists of the following terms:
Load1146(x0, x0, x1)
Cond_Load1146(TRUE, x0, x1)
Load1221(x0, x1, x2)
Cond_Load1221(TRUE, x0, x1, x2)
Cond_Load12211(TRUE, x0, x1, x2)

(27) IDPNonInfProof (SOUND transformation)

The constraints were generated the following way:
The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that final constraints are written in bold face.


For Pair COND_LOAD1221(TRUE, i118[3], i119[3], i84[3]) → LOAD1221(+(i118[3], -1), +(i119[3], -1), i84[3]) the following chains were created:
  • We consider the chain LOAD1221(i118[2], i119[2], i84[2]) → COND_LOAD1221(&&(>=(i84[2], 0), >(i119[2], i84[2])), i118[2], i119[2], i84[2]), COND_LOAD1221(TRUE, i118[3], i119[3], i84[3]) → LOAD1221(+(i118[3], -1), +(i119[3], -1), i84[3]), LOAD1221(i118[2], i119[2], i84[2]) → COND_LOAD1221(&&(>=(i84[2], 0), >(i119[2], i84[2])), i118[2], i119[2], i84[2]) which results in the following constraint:

    (1)    (&&(>=(i84[2], 0), >(i119[2], i84[2]))=TRUE∧i119[2]=i119[3]∧i84[2]=i84[3]∧i118[2]=i118[3]∧+(i119[3], -1)=i119[2]1∧+(i118[3], -1)=i118[2]1∧i84[3]=i84[2]1 ⇒ COND_LOAD1221(TRUE, i118[3], i119[3], i84[3])≥NonInfC∧COND_LOAD1221(TRUE, i118[3], i119[3], i84[3])≥LOAD1221(+(i118[3], -1), +(i119[3], -1), i84[3])∧(UIncreasing(LOAD1221(+(i118[3], -1), +(i119[3], -1), i84[3])), ≥))



    We simplified constraint (1) using rules (III), (IV), (IDP_BOOLEAN) which results in the following new constraint:

    (2)    (>=(i84[2], 0)=TRUE∧>(i119[2], i84[2])=TRUE ⇒ COND_LOAD1221(TRUE, i118[2], i119[2], i84[2])≥NonInfC∧COND_LOAD1221(TRUE, i118[2], i119[2], i84[2])≥LOAD1221(+(i118[2], -1), +(i119[2], -1), i84[2])∧(UIncreasing(LOAD1221(+(i118[3], -1), +(i119[3], -1), i84[3])), ≥))



    We simplified constraint (2) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (3)    (i84[2] ≥ 0∧i119[2] + [-1] + [-1]i84[2] ≥ 0 ⇒ (UIncreasing(LOAD1221(+(i118[3], -1), +(i119[3], -1), i84[3])), ≥)∧[(-1)bni_15 + (-1)Bound*bni_15] + [bni_15]i84[2] + [bni_15]i119[2] ≥ 0∧[1 + (-1)bso_16] ≥ 0)



    We simplified constraint (3) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (4)    (i84[2] ≥ 0∧i119[2] + [-1] + [-1]i84[2] ≥ 0 ⇒ (UIncreasing(LOAD1221(+(i118[3], -1), +(i119[3], -1), i84[3])), ≥)∧[(-1)bni_15 + (-1)Bound*bni_15] + [bni_15]i84[2] + [bni_15]i119[2] ≥ 0∧[1 + (-1)bso_16] ≥ 0)



    We simplified constraint (4) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (5)    (i84[2] ≥ 0∧i119[2] + [-1] + [-1]i84[2] ≥ 0 ⇒ (UIncreasing(LOAD1221(+(i118[3], -1), +(i119[3], -1), i84[3])), ≥)∧[(-1)bni_15 + (-1)Bound*bni_15] + [bni_15]i84[2] + [bni_15]i119[2] ≥ 0∧[1 + (-1)bso_16] ≥ 0)



    We simplified constraint (5) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

    (6)    (i84[2] ≥ 0∧i119[2] + [-1] + [-1]i84[2] ≥ 0 ⇒ (UIncreasing(LOAD1221(+(i118[3], -1), +(i119[3], -1), i84[3])), ≥)∧0 = 0∧[(-1)bni_15 + (-1)Bound*bni_15] + [bni_15]i84[2] + [bni_15]i119[2] ≥ 0∧0 = 0∧[1 + (-1)bso_16] ≥ 0)



    We simplified constraint (6) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (7)    (i84[2] ≥ 0∧i119[2] ≥ 0 ⇒ (UIncreasing(LOAD1221(+(i118[3], -1), +(i119[3], -1), i84[3])), ≥)∧0 = 0∧[(-1)Bound*bni_15] + [(2)bni_15]i84[2] + [bni_15]i119[2] ≥ 0∧0 = 0∧[1 + (-1)bso_16] ≥ 0)







For Pair LOAD1221(i118[2], i119[2], i84[2]) → COND_LOAD1221(&&(>=(i84[2], 0), >(i119[2], i84[2])), i118[2], i119[2], i84[2]) the following chains were created:
  • We consider the chain LOAD1221(i118[2], i119[2], i84[2]) → COND_LOAD1221(&&(>=(i84[2], 0), >(i119[2], i84[2])), i118[2], i119[2], i84[2]), COND_LOAD1221(TRUE, i118[3], i119[3], i84[3]) → LOAD1221(+(i118[3], -1), +(i119[3], -1), i84[3]) which results in the following constraint:

    (8)    (&&(>=(i84[2], 0), >(i119[2], i84[2]))=TRUE∧i119[2]=i119[3]∧i84[2]=i84[3]∧i118[2]=i118[3] ⇒ LOAD1221(i118[2], i119[2], i84[2])≥NonInfC∧LOAD1221(i118[2], i119[2], i84[2])≥COND_LOAD1221(&&(>=(i84[2], 0), >(i119[2], i84[2])), i118[2], i119[2], i84[2])∧(UIncreasing(COND_LOAD1221(&&(>=(i84[2], 0), >(i119[2], i84[2])), i118[2], i119[2], i84[2])), ≥))



    We simplified constraint (8) using rules (IV), (IDP_BOOLEAN) which results in the following new constraint:

    (9)    (>=(i84[2], 0)=TRUE∧>(i119[2], i84[2])=TRUE ⇒ LOAD1221(i118[2], i119[2], i84[2])≥NonInfC∧LOAD1221(i118[2], i119[2], i84[2])≥COND_LOAD1221(&&(>=(i84[2], 0), >(i119[2], i84[2])), i118[2], i119[2], i84[2])∧(UIncreasing(COND_LOAD1221(&&(>=(i84[2], 0), >(i119[2], i84[2])), i118[2], i119[2], i84[2])), ≥))



    We simplified constraint (9) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (10)    (i84[2] ≥ 0∧i119[2] + [-1] + [-1]i84[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1221(&&(>=(i84[2], 0), >(i119[2], i84[2])), i118[2], i119[2], i84[2])), ≥)∧[(-1)bni_17 + (-1)Bound*bni_17] + [bni_17]i84[2] + [bni_17]i119[2] ≥ 0∧[(-1)bso_18] ≥ 0)



    We simplified constraint (10) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (11)    (i84[2] ≥ 0∧i119[2] + [-1] + [-1]i84[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1221(&&(>=(i84[2], 0), >(i119[2], i84[2])), i118[2], i119[2], i84[2])), ≥)∧[(-1)bni_17 + (-1)Bound*bni_17] + [bni_17]i84[2] + [bni_17]i119[2] ≥ 0∧[(-1)bso_18] ≥ 0)



    We simplified constraint (11) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (12)    (i84[2] ≥ 0∧i119[2] + [-1] + [-1]i84[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1221(&&(>=(i84[2], 0), >(i119[2], i84[2])), i118[2], i119[2], i84[2])), ≥)∧[(-1)bni_17 + (-1)Bound*bni_17] + [bni_17]i84[2] + [bni_17]i119[2] ≥ 0∧[(-1)bso_18] ≥ 0)



    We simplified constraint (12) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

    (13)    (i84[2] ≥ 0∧i119[2] + [-1] + [-1]i84[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1221(&&(>=(i84[2], 0), >(i119[2], i84[2])), i118[2], i119[2], i84[2])), ≥)∧0 = 0∧[(-1)bni_17 + (-1)Bound*bni_17] + [bni_17]i84[2] + [bni_17]i119[2] ≥ 0∧0 = 0∧[(-1)bso_18] ≥ 0)



    We simplified constraint (13) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (14)    (i84[2] ≥ 0∧i119[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1221(&&(>=(i84[2], 0), >(i119[2], i84[2])), i118[2], i119[2], i84[2])), ≥)∧0 = 0∧[(-1)Bound*bni_17] + [(2)bni_17]i84[2] + [bni_17]i119[2] ≥ 0∧0 = 0∧[(-1)bso_18] ≥ 0)







To summarize, we get the following constraints P≥ for the following pairs.
  • COND_LOAD1221(TRUE, i118[3], i119[3], i84[3]) → LOAD1221(+(i118[3], -1), +(i119[3], -1), i84[3])
    • (i84[2] ≥ 0∧i119[2] ≥ 0 ⇒ (UIncreasing(LOAD1221(+(i118[3], -1), +(i119[3], -1), i84[3])), ≥)∧0 = 0∧[(-1)Bound*bni_15] + [(2)bni_15]i84[2] + [bni_15]i119[2] ≥ 0∧0 = 0∧[1 + (-1)bso_16] ≥ 0)

  • LOAD1221(i118[2], i119[2], i84[2]) → COND_LOAD1221(&&(>=(i84[2], 0), >(i119[2], i84[2])), i118[2], i119[2], i84[2])
    • (i84[2] ≥ 0∧i119[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1221(&&(>=(i84[2], 0), >(i119[2], i84[2])), i118[2], i119[2], i84[2])), ≥)∧0 = 0∧[(-1)Bound*bni_17] + [(2)bni_17]i84[2] + [bni_17]i119[2] ≥ 0∧0 = 0∧[(-1)bso_18] ≥ 0)




The constraints for P> respective Pbound are constructed from P≥ where we just replace every occurence of "t ≥ s" in P≥ by "t > s" respective "t ≥ c". Here c stands for the fresh constant used for Pbound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation over integers[POLO]:

POL(TRUE) = 0   
POL(FALSE) = [1]   
POL(COND_LOAD1221(x1, x2, x3, x4)) = [-1] + x4 + x3   
POL(LOAD1221(x1, x2, x3)) = [-1] + x3 + x2   
POL(+(x1, x2)) = x1 + x2   
POL(-1) = [-1]   
POL(&&(x1, x2)) = [-1]   
POL(>=(x1, x2)) = [-1]   
POL(0) = 0   
POL(>(x1, x2)) = [-1]   

The following pairs are in P>:

COND_LOAD1221(TRUE, i118[3], i119[3], i84[3]) → LOAD1221(+(i118[3], -1), +(i119[3], -1), i84[3])

The following pairs are in Pbound:

COND_LOAD1221(TRUE, i118[3], i119[3], i84[3]) → LOAD1221(+(i118[3], -1), +(i119[3], -1), i84[3])
LOAD1221(i118[2], i119[2], i84[2]) → COND_LOAD1221(&&(>=(i84[2], 0), >(i119[2], i84[2])), i118[2], i119[2], i84[2])

The following pairs are in P≥:

LOAD1221(i118[2], i119[2], i84[2]) → COND_LOAD1221(&&(>=(i84[2], 0), >(i119[2], i84[2])), i118[2], i119[2], i84[2])

At least the following rules have been oriented under context sensitive arithmetic replacement:

TRUE1 → &&(TRUE, TRUE)1
FALSE1 → &&(TRUE, FALSE)1
FALSE1 → &&(FALSE, TRUE)1
FALSE1 → &&(FALSE, FALSE)1

(28) Complex Obligation (AND)

(29) Obligation:

IDP problem:
The following function symbols are pre-defined:
!=~Neq: (Integer, Integer) -> Boolean
*~Mul: (Integer, Integer) -> Integer
>=~Ge: (Integer, Integer) -> Boolean
-1~UnaryMinus: (Integer) -> Integer
|~Bwor: (Integer, Integer) -> Integer
/~Div: (Integer, Integer) -> Integer
=~Eq: (Integer, Integer) -> Boolean
~Bwxor: (Integer, Integer) -> Integer
||~Lor: (Boolean, Boolean) -> Boolean
!~Lnot: (Boolean) -> Boolean
<~Lt: (Integer, Integer) -> Boolean
-~Sub: (Integer, Integer) -> Integer
<=~Le: (Integer, Integer) -> Boolean
>~Gt: (Integer, Integer) -> Boolean
~~Bwnot: (Integer) -> Integer
%~Mod: (Integer, Integer) -> Integer
&~Bwand: (Integer, Integer) -> Integer
+~Add: (Integer, Integer) -> Integer
&&~Land: (Boolean, Boolean) -> Boolean


The following domains are used:

Boolean, Integer


R is empty.

The integer pair graph contains the following rules and edges:
(2): LOAD1221(i118[2], i119[2], i84[2]) → COND_LOAD1221(i84[2] >= 0 && i119[2] > i84[2], i118[2], i119[2], i84[2])


The set Q consists of the following terms:
Load1146(x0, x0, x1)
Cond_Load1146(TRUE, x0, x1)
Load1221(x0, x1, x2)
Cond_Load1221(TRUE, x0, x1, x2)
Cond_Load12211(TRUE, x0, x1, x2)

(30) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.

(31) TRUE

(32) Obligation:

IDP problem:
The following function symbols are pre-defined:
!=~Neq: (Integer, Integer) -> Boolean
*~Mul: (Integer, Integer) -> Integer
>=~Ge: (Integer, Integer) -> Boolean
-1~UnaryMinus: (Integer) -> Integer
|~Bwor: (Integer, Integer) -> Integer
/~Div: (Integer, Integer) -> Integer
=~Eq: (Integer, Integer) -> Boolean
~Bwxor: (Integer, Integer) -> Integer
||~Lor: (Boolean, Boolean) -> Boolean
!~Lnot: (Boolean) -> Boolean
<~Lt: (Integer, Integer) -> Boolean
-~Sub: (Integer, Integer) -> Integer
<=~Le: (Integer, Integer) -> Boolean
>~Gt: (Integer, Integer) -> Boolean
~~Bwnot: (Integer) -> Integer
%~Mod: (Integer, Integer) -> Integer
&~Bwand: (Integer, Integer) -> Integer
+~Add: (Integer, Integer) -> Integer
&&~Land: (Boolean, Boolean) -> Boolean


The following domains are used:
none


R is empty.

The integer pair graph is empty.

The set Q consists of the following terms:
Load1146(x0, x0, x1)
Cond_Load1146(TRUE, x0, x1)
Load1221(x0, x1, x2)
Cond_Load1221(TRUE, x0, x1, x2)
Cond_Load12211(TRUE, x0, x1, x2)

(33) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs.

(34) TRUE